0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 11 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 234 ms)
↳12 BOUNDS(1, 1)
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(n__add(sqr(activate(X)), dbl(activate(X))))
dbl(0) → 0
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
add(0, X) → X
add(s(X), Y) → s(n__add(activate(X), Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z)))
terms(X) → n__terms(X)
add(X1, X2) → n__add(X1, X2)
s(X) → n__s(X)
dbl(X) → n__dbl(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(X)
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__s(X)) → s(X)
activate(n__dbl(X)) → dbl(X)
activate(n__first(X1, X2)) → first(X1, X2)
activate(X) → X
dbl(0) → 0
terms(X) → n__terms(X)
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
first(0, X) → nil
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__dbl(X)) → dbl(X)
activate(X) → X
add(X1, X2) → n__add(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__terms(X)) → terms(X)
sqr(0) → 0
add(0, X) → X
first(X1, X2) → n__first(X1, X2)
dbl(X) → n__dbl(X)
s(X) → n__s(X)
activate(n__s(X)) → s(X)
dbl(0) → 0 [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1]
first(0, X) → nil [1]
activate(n__add(X1, X2)) → add(X1, X2) [1]
activate(n__dbl(X)) → dbl(X) [1]
activate(X) → X [1]
add(X1, X2) → n__add(X1, X2) [1]
activate(n__first(X1, X2)) → first(X1, X2) [1]
activate(n__terms(X)) → terms(X) [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
first(X1, X2) → n__first(X1, X2) [1]
dbl(X) → n__dbl(X) [1]
s(X) → n__s(X) [1]
activate(n__s(X)) → s(X) [1]
dbl(0) → 0 [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1]
first(0, X) → nil [1]
activate(n__add(X1, X2)) → add(X1, X2) [1]
activate(n__dbl(X)) → dbl(X) [1]
activate(X) → X [1]
add(X1, X2) → n__add(X1, X2) [1]
activate(n__first(X1, X2)) → first(X1, X2) [1]
activate(n__terms(X)) → terms(X) [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
first(X1, X2) → n__first(X1, X2) [1]
dbl(X) → n__dbl(X) [1]
s(X) → n__s(X) [1]
activate(n__s(X)) → s(X) [1]
| dbl :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s 0 :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s terms :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s n__terms :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s cons :: recip → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s recip :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → recip sqr :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s s :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s first :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → a → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s nil :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s activate :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s n__add :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s add :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s n__dbl :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s n__first :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → a → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s n__s :: 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s → 0:n__terms:cons:nil:n__add:n__dbl:n__first:n__s |
sqr(v0) → null_sqr [0]
null_sqr, const, const1
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
nil => 1
null_sqr => 0
const => 0
const1 => 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ terms(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ dbl(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ add(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + s(N)) :|: z = N, N >= 0
| eq(start(V, V1),0,[dbl(V, Out)],[V >= 0]). eq(start(V, V1),0,[terms(V, Out)],[V >= 0]). eq(start(V, V1),0,[first(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[activate(V, Out)],[V >= 0]). eq(start(V, V1),0,[add(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[sqr(V, Out)],[V >= 0]). eq(start(V, V1),0,[s(V, Out)],[V >= 0]). eq(dbl(V, Out),1,[],[Out = 0,V = 0]). eq(terms(V, Out),1,[],[Out = 1 + X3,X3 >= 0,V = X3]). eq(terms(V, Out),1,[sqr(N1, Ret011),s(N1, Ret11)],[Out = 3 + Ret011 + Ret11,V = N1,N1 >= 0]). eq(first(V, V1, Out),1,[],[Out = 1,V1 = X4,X4 >= 0,V = 0]). eq(activate(V, Out),1,[add(X11, X21, Ret)],[Out = Ret,X11 >= 0,X21 >= 0,V = 1 + X11 + X21]). eq(activate(V, Out),1,[dbl(X5, Ret1)],[Out = Ret1,V = 1 + X5,X5 >= 0]). eq(activate(V, Out),1,[],[Out = X6,X6 >= 0,V = X6]). eq(add(V, V1, Out),1,[],[Out = 1 + X12 + X22,X12 >= 0,X22 >= 0,V = X12,V1 = X22]). eq(activate(V, Out),1,[first(X13, X23, Ret2)],[Out = Ret2,X13 >= 0,X23 >= 0,V = 1 + X13 + X23]). eq(activate(V, Out),1,[terms(X7, Ret3)],[Out = Ret3,V = 1 + X7,X7 >= 0]). eq(sqr(V, Out),1,[],[Out = 0,V = 0]). eq(add(V, V1, Out),1,[],[Out = X8,V1 = X8,X8 >= 0,V = 0]). eq(first(V, V1, Out),1,[],[Out = 1 + X14 + X24,X14 >= 0,X24 >= 0,V = X14,V1 = X24]). eq(dbl(V, Out),1,[],[Out = 1 + X9,X9 >= 0,V = X9]). eq(s(V, Out),1,[],[Out = 1 + X10,X10 >= 0,V = X10]). eq(activate(V, Out),1,[s(X15, Ret4)],[Out = Ret4,V = 1 + X15,X15 >= 0]). eq(sqr(V, Out),0,[],[Out = 0,V2 >= 0,V = V2]). input_output_vars(dbl(V,Out),[V],[Out]). input_output_vars(terms(V,Out),[V],[Out]). input_output_vars(first(V,V1,Out),[V,V1],[Out]). input_output_vars(activate(V,Out),[V],[Out]). input_output_vars(add(V,V1,Out),[V,V1],[Out]). input_output_vars(sqr(V,Out),[V],[Out]). input_output_vars(s(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [add/3]
1. non_recursive : [dbl/2]
2. non_recursive : [first/3]
3. non_recursive : [s/2]
4. non_recursive : [sqr/2]
5. non_recursive : [terms/2]
6. non_recursive : [activate/2]
7. non_recursive : [start/2]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into add/3
1. SCC is partially evaluated into dbl/2
2. SCC is partially evaluated into first/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into sqr/2
5. SCC is partially evaluated into terms/2
6. SCC is partially evaluated into activate/2
7. SCC is partially evaluated into start/2
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations add/3
* CE 21 is refined into CE [25]
* CE 22 is refined into CE [26]
### Cost equations --> "Loop" of add/3
* CEs [25] --> Loop 12
* CEs [26] --> Loop 13
### Ranking functions of CR add(V,V1,Out)
#### Partial ranking functions of CR add(V,V1,Out)
### Specialization of cost equations dbl/2
* CE 10 is refined into CE [27]
* CE 9 is refined into CE [28]
### Cost equations --> "Loop" of dbl/2
* CEs [27] --> Loop 14
* CEs [28] --> Loop 15
### Ranking functions of CR dbl(V,Out)
#### Partial ranking functions of CR dbl(V,Out)
### Specialization of cost equations first/3
* CE 14 is refined into CE [29]
* CE 13 is refined into CE [30]
### Cost equations --> "Loop" of first/3
* CEs [29] --> Loop 16
* CEs [30] --> Loop 17
### Ranking functions of CR first(V,V1,Out)
#### Partial ranking functions of CR first(V,V1,Out)
### Specialization of cost equations sqr/2
* CE 23 is refined into CE [31]
* CE 24 is refined into CE [32]
### Cost equations --> "Loop" of sqr/2
* CEs [31,32] --> Loop 18
### Ranking functions of CR sqr(V,Out)
#### Partial ranking functions of CR sqr(V,Out)
### Specialization of cost equations terms/2
* CE 11 is refined into CE [33]
* CE 12 is refined into CE [34]
### Cost equations --> "Loop" of terms/2
* CEs [33] --> Loop 19
* CEs [34] --> Loop 20
### Ranking functions of CR terms(V,Out)
#### Partial ranking functions of CR terms(V,Out)
### Specialization of cost equations activate/2
* CE 15 is refined into CE [35,36]
* CE 16 is refined into CE [37,38]
* CE 18 is refined into CE [39,40]
* CE 19 is refined into CE [41,42]
* CE 17 is refined into CE [43]
* CE 20 is refined into CE [44]
### Cost equations --> "Loop" of activate/2
* CEs [36,38,40,42,43,44] --> Loop 21
* CEs [41] --> Loop 22
* CEs [39] --> Loop 23
* CEs [35,37] --> Loop 24
### Ranking functions of CR activate(V,Out)
#### Partial ranking functions of CR activate(V,Out)
### Specialization of cost equations start/2
* CE 2 is refined into CE [45,46]
* CE 3 is refined into CE [47,48]
* CE 4 is refined into CE [49,50]
* CE 5 is refined into CE [51,52,53,54]
* CE 6 is refined into CE [55,56]
* CE 7 is refined into CE [57]
* CE 8 is refined into CE [58]
### Cost equations --> "Loop" of start/2
* CEs [45,46,47,48,49,50,51,52,53,54,55,56,57,58] --> Loop 25
### Ranking functions of CR start(V,V1)
#### Partial ranking functions of CR start(V,V1)
Computing Bounds
=====================================
#### Cost of chains of add(V,V1,Out):
* Chain [13]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [12]: 1
with precondition: [V+V1+1=Out,V>=0,V1>=0]
#### Cost of chains of dbl(V,Out):
* Chain [15]: 1
with precondition: [V=0,Out=0]
* Chain [14]: 1
with precondition: [V+1=Out,V>=0]
#### Cost of chains of first(V,V1,Out):
* Chain [17]: 1
with precondition: [V=0,Out=1,V1>=0]
* Chain [16]: 1
with precondition: [V+V1+1=Out,V>=0,V1>=0]
#### Cost of chains of sqr(V,Out):
* Chain [18]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of terms(V,Out):
* Chain [20]: 3
with precondition: [V+4=Out,V>=0]
* Chain [19]: 1
with precondition: [V+1=Out,V>=0]
#### Cost of chains of activate(V,Out):
* Chain [24]: 2
with precondition: [V=Out+1,V>=1]
* Chain [23]: 2
with precondition: [Out=1,V>=1]
* Chain [22]: 4
with precondition: [V+3=Out,V>=1]
* Chain [21]: 2
with precondition: [V=Out,V>=0]
#### Cost of chains of start(V,V1):
* Chain [25]: 4
with precondition: [V>=0]
Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [25] with precondition: [V>=0]
- Upper bound: 4
- Complexity: constant
### Maximum cost of start(V,V1): 4
Asymptotic class: constant
* Total analysis performed in 133 ms.